The problem is undecidable and even practical instances are challenging. Inspired by how human experts construct loop invariants, we propose a reasoning framework Code2Inv that constructs the solution by multi-step decision making and querying an external program graph memory block. By training with reinforcement learning, Code2Inv captures rich program features and avoids the need for ground truth solutions as supervision. Compared to previous learning tasks in domains with graph-structured data, it addresses unique challenges, such as a binary objective function and an extremely sparse reward that is given by an automated theorem prover only after the complete loop invariant is proposed. We evaluate Code2Inv on a suite of 133 benchmark problems and compare it to three state-of-the-art systems. It solves 106 problems compared to 73 by a stochastic search-based system, 77 by a heuristic search-based system, and 100 by a decision tree learning-based system. Moreover, the strategy learned can be generalized to new programs: compared to solving new instances from scratch, the pre-trained agent is more sample efficient in finding solutions.

The paper presents a novel deep network architecture termed DELPHI to automatically infer loop invariants for use in program verification. The architecture takes in as input source code which has (1) a number of assumption or assignment statements, (2) a loop with nested if-else statements with arithmetic operations and (3) a final assertion statement. The output of the architecture is a loop invariant in CNF which holds true at every iteration in the loop, and for which the assertion (3) is true after the loop ends execution. The architecture represents the source code AST using a graph-structured neural network, and treats it as a structured memory which it repeatedly accesses through attention operations. The generation of the CNF invariant is broken up into a sequential decision-making process where at each time the architecture predicts an output (op, T), where op is either && or and T is a simple logical expression.

The problem is undecidable and even practical instances are challenging. Inspired by how human experts construct loop invariants, we propose a reasoning framework Code2Inv that constructs the solution by multi-step decision making and querying an external program graph memory block. By training with reinforcement learning, Code2Inv captures rich program features and avoids the need for ground truth solutions as supervision. Compared to previous learning tasks in domains with graph-structured data, it addresses unique challenges, such as a binary objective function and an extremely sparse reward that is given by an automated theorem prover only after the complete loop invariant is proposed. We evaluate Code2Inv on a suite of 133 benchmark problems and compare it to three state-of-the-art systems.